CALM Theorem
このモデルでは、特定のプログラムの結果の一貫性に、Coordinationが必要かどうかの議論を曖昧にしていた
どのようなProblemであっても、Coordinationを必要としない解があるのか、それとも必要なのかをどうやって知ることができるのか?
アナロジー: 交差点問題。一時停止の信号をどう制御するかに腐心しなくても、片方の道にトンネルを掘れば信号自体をなくすことができる
Coordination-freeなComputational Problem: Coordinationを使わずに一貫性のある出力を計算することができる分散実装が存在するComputational problem どのような問題群はCoordination-freeなのか? そしてどのような問題群はその外に位置するのか?
Coordination-freeでない例: Distributed GCでは、Rootからの参照グラフ全体が見えないとObjectの参照が一切ないことがわからないので、捨てられない。グラフ全体を知るためにCoordinationが必要 Def 1. A problem P is monotonic if for any input sets $ S, $ T where $ S \subseteq T $ P(S) \subseteq P(T) Theorem 1. Consistency As Logical Monotonicity (CALM): A problem has a consistent, corrdination-free distributed implementation if and only if it is monotonic
monotonicである場合、かつその場合に限り、問題は一貫性のある、Coordination-freeな分散実装を持つ
直感的には、monotonicな問題は、情報(Input)が欠落していても安全であり、協調無しで進めることができる。逆に非monotonicな問題は、新しい情報(Input)に直面したときにある性質の真理が変化することを懸念しなければならない。したがって、すべての情報が到着したことを知るまで先に進めない
monotonicな問題は、inputの到着順序に依存しない。non-monotonicな問題は、入力の順序で出力が変わる
操作
Ingest and apply: 順序付けされていないリクエスト(レコード挿入・削除)のバッチを読み込んで、適用する
Query: ローカルのRelation(レコードの集合)をクエリして、計算処理を行う 例えば、$ \neg\exists x : P(x)というクエリが一時的に真でも、あとから追加で$ P(x)を満たす$ xがやってきて、偽になるかもしれない。これはmonotonicityを満たさないkekeho.icon
Send: クエリの結果をローカル・他マシンに送る
Theorem 1のifの証明の概要: monotonicなRelational transducerのネットワークでは、最終的に決定論的な入力を得て、決定論的な出力を生成する。また、実行中の任意の時点において、$ P(S) \subseteq T(S)。 only ifの証明:
メッセージを、Relational transducerのデータフローメッセージと、他のCoordinationに使うメッセージを分けて議論を進める。 仮にデータが1箇所にすべて集められているとして、それでも送られるデータってのはCoordination message。だって明らかにデータフロー以外の目的(=Coordination)に使われているからkekeho.icon うーんそうっすけど、でもほんとに? 納得感があまりないkekeho.icon
非単調操作が常にCoordination messageを送る必要があることを証明する
ここ具体的にどう証明するんだろう。証明した論文を読まねばkekeho.icon
メモ
CALMは、CAP定理のC,A,Pが同時に満たせる問題のクラスを規定する パーティションから回復するとき、状態のマージはmonotonicであり、一貫している
たしかに!kekeho.icon
うーん、やっぱりCが違うから比べて良いのかな?kekeho.icon
うんちく
PODS 2010で予想が発表されて、amelootらが色々形式化とか証明とかをした 参考資料
Communications of the ACMの記事
証明した論文